(include-book "../src/acl2/frame-stepper")
(include-book "../src/acl2/grid")
(include-book "../src/acl2/rule-creator")
(include-book "../src/acl2/cell")
(include-book "generators/grid-data-generator")
(include-book "generators/rule-creator-data-generator")
;;;Tests for the framestepper module

;;Horizontal bar pattern used in a check-expect
(defconst *horiz-bar*
	(lifelike-grid-set (lifelike-grid-set 
		(lifelike-grid-set (empty-lifelike-grid)
		 0 0 t) 1 0 t) -1 0 t))

;;Vertical bar for a check-expect
(defconst *vertical-bar*
	(lifelike-grid-set (lifelike-grid-set 
		(lifelike-grid-set (empty-lifelike-grid)
		 0 0 t) 0 1 t) 0 -1 t))

;;Used in a check-expect. 
;;birth states = 3,
;;death states = everything besides 2 and 3.
(defconst *game-of-life-rules*
	(generate-lifelike-rules* 
		(list 0 1 4 5 6 7 8) (list 3)))

;;Used in a check-expect
(defconst *elem* 
    (elementary-grid-set
	    (elementary-grid-set 
	     (elementary-grid-set (empty-elementary-grid) 4 t)
	     -9 t)
      	22 t))
	
;;Check that the frame stepper will turn a horizontal
;;bar into a vertical bar with lifelike rules.
(check-expect (car (grid-step *horiz-bar* *game-of-life-rules*))
	*vertical-bar*)

;;Check that the frame stepper will turn a vertical
;;bar into a horizontal bar with lifelike rules.
(check-expect (car (grid-step *vertical-bar* *game-of-life-rules*))
	*horiz-bar*)

;;Check bounds
(check-expect (get-ll-bounds *vertical-bar*)
      (ll-bounds 0 0 1 -1))
(check-expect (get-ll-bounds *horiz-bar*)
      (ll-bounds -1 1 0 0))
(check-expect (get-el-bounds *elem*)
      (el-bounds -9 22))


;;Given a random grid with particular size and
;;random (valid) rules, and a random cell in the
;;grid, check that the cell corresponds to
;; the next state in the rules for lifelike rules
(defproperty test-check-lifelike-cell*
	(grid :value (random-lifelike-grid 10 10 0.2)
	 birth-rules :value (random-birth-state-list)
	 death-rules :value (random-death-state-list)
	 rules :value (generate-lifelike-rules* death-rules birth-rules)
	 cell-x :value (random-between -9 9)
	 cell-y :value (random-between -9 9)
         next :value (car (grid-step grid rules))
	chosen-cell :value (cell cell-x cell-y)
	cell-value :value (lifelike-grid-get grid cell-x cell-y)
        cell-neighbors :value (get-lifelike-neighbors-live-count* grid chosen-cell)
	expected-value :value (if cell-value
                                  (if (member-equal cell-neighbors death-rules)
                                      nil
                                      t)
                                  (if (member-equal cell-neighbors birth-rules)
                                      t
                                      nil))
        val :value (lifelike-grid-get next cell-x cell-y))
		  (equal val expected-value))



;;Given a random grid with particular size and
;;random (valid) rules, and a random cell in the
;;grid, check that the cell corresponds to
;; the next state in the rules for elementary rules
(defproperty test-check-elementary-cell*
	(grid :value (random-elementary-grid 50 0.5)
	 wolfram-code :value (random-wolfram-code)
	 rules :value (generate-elementary-rules* wolfram-code)
	 cell-pos :value (random-between 0 49)
     cell-value :value (elementary-grid-get grid cell-pos)
     wolf-table :value (parse-wolfram-code wolfram-code)
     sitno :value (get-situation-number grid cell-pos)
     expected-value :value (check-situation wolf-table sitno)
     next-grid :value (car (grid-step grid rules))
     real-value :value (elementary-grid-get next-grid cell-pos))
	  (equal real-value
	  		expected-value))
			  